n:, i:. exp(i;n)   

latex

Definitions	t  T, #$n, a < b, x:A. B(x), primrec(n;b;c), n * m, , {x:A| B(x)} , , A  B, n - m, -n, n+m, Void, x:AB(x), P  Q, False, A, , {i..j}, x.A(x), (i = j), if b then t else f fi , exp(i;n), i  j , i > j, P  Q, P & Q, P  Q
Lemmas	pos mul arg bounds, ge wf, nat properties, nat wf, ifthenelse wf, eq int wf, nat plus wf, primrec wf, int seg wf, le wf